Left Termination of the query pattern at_in_2(a, a) w.r.t. the given Prolog program could successfully be proven:



Prolog
  ↳ PrologToPiTRSProof

Clauses:

at(X, fido) :- ','(at(X, mary), near(X)).
at(ta, mary).
at(jm, mary).
near(jm).

Queries:

at(a,a).

We use the technique of [30]. With regard to the inferred argument filtering the predicates were used in the following modes:
at_in: (f,f) (f,b)
Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

at_in_aa(X, fido) → U1_aa(X, at_in_ag(X, mary))
at_in_ag(X, fido) → U1_ag(X, at_in_ag(X, mary))
at_in_ag(ta, mary) → at_out_ag(ta, mary)
at_in_ag(jm, mary) → at_out_ag(jm, mary)
U1_ag(X, at_out_ag(X, mary)) → U2_ag(X, near_in_g(X))
near_in_g(jm) → near_out_g(jm)
U2_ag(X, near_out_g(X)) → at_out_ag(X, fido)
U1_aa(X, at_out_ag(X, mary)) → U2_aa(X, near_in_g(X))
U2_aa(X, near_out_g(X)) → at_out_aa(X, fido)
at_in_aa(ta, mary) → at_out_aa(ta, mary)
at_in_aa(jm, mary) → at_out_aa(jm, mary)

The argument filtering Pi contains the following mapping:
at_in_aa(x1, x2)  =  at_in_aa
U1_aa(x1, x2)  =  U1_aa(x2)
at_in_ag(x1, x2)  =  at_in_ag(x2)
fido  =  fido
U1_ag(x1, x2)  =  U1_ag(x2)
mary  =  mary
at_out_ag(x1, x2)  =  at_out_ag(x1)
U2_ag(x1, x2)  =  U2_ag(x1, x2)
near_in_g(x1)  =  near_in_g(x1)
jm  =  jm
near_out_g(x1)  =  near_out_g
U2_aa(x1, x2)  =  U2_aa(x1, x2)
at_out_aa(x1, x2)  =  at_out_aa(x1, x2)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog



↳ Prolog
  ↳ PrologToPiTRSProof
PiTRS
      ↳ DependencyPairsProof

Pi-finite rewrite system:
The TRS R consists of the following rules:

at_in_aa(X, fido) → U1_aa(X, at_in_ag(X, mary))
at_in_ag(X, fido) → U1_ag(X, at_in_ag(X, mary))
at_in_ag(ta, mary) → at_out_ag(ta, mary)
at_in_ag(jm, mary) → at_out_ag(jm, mary)
U1_ag(X, at_out_ag(X, mary)) → U2_ag(X, near_in_g(X))
near_in_g(jm) → near_out_g(jm)
U2_ag(X, near_out_g(X)) → at_out_ag(X, fido)
U1_aa(X, at_out_ag(X, mary)) → U2_aa(X, near_in_g(X))
U2_aa(X, near_out_g(X)) → at_out_aa(X, fido)
at_in_aa(ta, mary) → at_out_aa(ta, mary)
at_in_aa(jm, mary) → at_out_aa(jm, mary)

The argument filtering Pi contains the following mapping:
at_in_aa(x1, x2)  =  at_in_aa
U1_aa(x1, x2)  =  U1_aa(x2)
at_in_ag(x1, x2)  =  at_in_ag(x2)
fido  =  fido
U1_ag(x1, x2)  =  U1_ag(x2)
mary  =  mary
at_out_ag(x1, x2)  =  at_out_ag(x1)
U2_ag(x1, x2)  =  U2_ag(x1, x2)
near_in_g(x1)  =  near_in_g(x1)
jm  =  jm
near_out_g(x1)  =  near_out_g
U2_aa(x1, x2)  =  U2_aa(x1, x2)
at_out_aa(x1, x2)  =  at_out_aa(x1, x2)


Using Dependency Pairs [1,30] we result in the following initial DP problem:
Pi DP problem:
The TRS P consists of the following rules:

AT_IN_AA(X, fido) → U1_AA(X, at_in_ag(X, mary))
AT_IN_AA(X, fido) → AT_IN_AG(X, mary)
AT_IN_AG(X, fido) → U1_AG(X, at_in_ag(X, mary))
AT_IN_AG(X, fido) → AT_IN_AG(X, mary)
U1_AG(X, at_out_ag(X, mary)) → U2_AG(X, near_in_g(X))
U1_AG(X, at_out_ag(X, mary)) → NEAR_IN_G(X)
U1_AA(X, at_out_ag(X, mary)) → U2_AA(X, near_in_g(X))
U1_AA(X, at_out_ag(X, mary)) → NEAR_IN_G(X)

The TRS R consists of the following rules:

at_in_aa(X, fido) → U1_aa(X, at_in_ag(X, mary))
at_in_ag(X, fido) → U1_ag(X, at_in_ag(X, mary))
at_in_ag(ta, mary) → at_out_ag(ta, mary)
at_in_ag(jm, mary) → at_out_ag(jm, mary)
U1_ag(X, at_out_ag(X, mary)) → U2_ag(X, near_in_g(X))
near_in_g(jm) → near_out_g(jm)
U2_ag(X, near_out_g(X)) → at_out_ag(X, fido)
U1_aa(X, at_out_ag(X, mary)) → U2_aa(X, near_in_g(X))
U2_aa(X, near_out_g(X)) → at_out_aa(X, fido)
at_in_aa(ta, mary) → at_out_aa(ta, mary)
at_in_aa(jm, mary) → at_out_aa(jm, mary)

The argument filtering Pi contains the following mapping:
at_in_aa(x1, x2)  =  at_in_aa
U1_aa(x1, x2)  =  U1_aa(x2)
at_in_ag(x1, x2)  =  at_in_ag(x2)
fido  =  fido
U1_ag(x1, x2)  =  U1_ag(x2)
mary  =  mary
at_out_ag(x1, x2)  =  at_out_ag(x1)
U2_ag(x1, x2)  =  U2_ag(x1, x2)
near_in_g(x1)  =  near_in_g(x1)
jm  =  jm
near_out_g(x1)  =  near_out_g
U2_aa(x1, x2)  =  U2_aa(x1, x2)
at_out_aa(x1, x2)  =  at_out_aa(x1, x2)
AT_IN_AG(x1, x2)  =  AT_IN_AG(x2)
U2_AG(x1, x2)  =  U2_AG(x1, x2)
U1_AA(x1, x2)  =  U1_AA(x2)
U2_AA(x1, x2)  =  U2_AA(x1, x2)
NEAR_IN_G(x1)  =  NEAR_IN_G(x1)
AT_IN_AA(x1, x2)  =  AT_IN_AA
U1_AG(x1, x2)  =  U1_AG(x2)

We have to consider all (P,R,Pi)-chains

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
PiDP
          ↳ DependencyGraphProof

Pi DP problem:
The TRS P consists of the following rules:

AT_IN_AA(X, fido) → U1_AA(X, at_in_ag(X, mary))
AT_IN_AA(X, fido) → AT_IN_AG(X, mary)
AT_IN_AG(X, fido) → U1_AG(X, at_in_ag(X, mary))
AT_IN_AG(X, fido) → AT_IN_AG(X, mary)
U1_AG(X, at_out_ag(X, mary)) → U2_AG(X, near_in_g(X))
U1_AG(X, at_out_ag(X, mary)) → NEAR_IN_G(X)
U1_AA(X, at_out_ag(X, mary)) → U2_AA(X, near_in_g(X))
U1_AA(X, at_out_ag(X, mary)) → NEAR_IN_G(X)

The TRS R consists of the following rules:

at_in_aa(X, fido) → U1_aa(X, at_in_ag(X, mary))
at_in_ag(X, fido) → U1_ag(X, at_in_ag(X, mary))
at_in_ag(ta, mary) → at_out_ag(ta, mary)
at_in_ag(jm, mary) → at_out_ag(jm, mary)
U1_ag(X, at_out_ag(X, mary)) → U2_ag(X, near_in_g(X))
near_in_g(jm) → near_out_g(jm)
U2_ag(X, near_out_g(X)) → at_out_ag(X, fido)
U1_aa(X, at_out_ag(X, mary)) → U2_aa(X, near_in_g(X))
U2_aa(X, near_out_g(X)) → at_out_aa(X, fido)
at_in_aa(ta, mary) → at_out_aa(ta, mary)
at_in_aa(jm, mary) → at_out_aa(jm, mary)

The argument filtering Pi contains the following mapping:
at_in_aa(x1, x2)  =  at_in_aa
U1_aa(x1, x2)  =  U1_aa(x2)
at_in_ag(x1, x2)  =  at_in_ag(x2)
fido  =  fido
U1_ag(x1, x2)  =  U1_ag(x2)
mary  =  mary
at_out_ag(x1, x2)  =  at_out_ag(x1)
U2_ag(x1, x2)  =  U2_ag(x1, x2)
near_in_g(x1)  =  near_in_g(x1)
jm  =  jm
near_out_g(x1)  =  near_out_g
U2_aa(x1, x2)  =  U2_aa(x1, x2)
at_out_aa(x1, x2)  =  at_out_aa(x1, x2)
AT_IN_AG(x1, x2)  =  AT_IN_AG(x2)
U2_AG(x1, x2)  =  U2_AG(x1, x2)
U1_AA(x1, x2)  =  U1_AA(x2)
U2_AA(x1, x2)  =  U2_AA(x1, x2)
NEAR_IN_G(x1)  =  NEAR_IN_G(x1)
AT_IN_AA(x1, x2)  =  AT_IN_AA
U1_AG(x1, x2)  =  U1_AG(x2)

We have to consider all (P,R,Pi)-chains
The approximation of the Dependency Graph [30] contains 0 SCCs with 8 less nodes.